T:Type, l1, l2, l3:(T List). fseg(T;l1;l2)  fseg(T;l2;l3)  fseg(T;l1;l3) 

latex

ProofTree

Definitions	Type, , t  T, s = t, x:AB(x), x:A. B(x), type List, , as @ bs, x:A  B(x), x:A. B(x), ||as||, {x:A| B(x)} , Top, S  T, , s ~ t, {T}, P  Q, SQType(T), [car / cdr], P & Q, P  Q, P  Q, A  B, i  j , Void, x:A.B(x), [], A List, fseg(T;L1;L2)
Lemmas	iff wf, rev implies wf, append assoc, non neg length, cons one one, guard wf, nat wf, length wf nat, top wf, append wf, member wf